|
System Fは型付きラムダ計算の一体系で，単純型付きラムダ計算に型についての全称量化を導入したものである．2階ラムダ計算や（ジラール–レイノルズ）多相ラムダ計算としても知られる．プログラミング言語におけるパラメータ多相を形式化するもので，MLやHaskellのような関数型言語の論理的な背景となっている．System Fは論理学者のジャン＝イヴ・ジラールおよび計算機科学者のジョン・C・レイノルズによって独立に発見された． 単純型付きラムダ計算では，関数についての変数とその束縛が存在するが，System Fでは''型''についての変数とその束縛が追加されている．例えば恒等関数は任意の型についての形の型を持ちうるが，System Fではこのことが次の判断が成り立つことによって表されている: :. ここで，は型変数である．また，小文字のが通常の値レベルの抽象を表しているのに対して，大文字のを型レベルの抽象を表すために使用している． 項書換え系として見ると，System Fは強正規化性を持つ．しかしながらSystem Fにおける型推論は決定不能である．またSystem Fはカリー＝ハワード同型の下で，全称量化のみを用いる2階直観主義論理の断片に対応する．System Fは依存型などを含んだより強力なラムダ計算とともに，ラムダ・キューブの一角であるとみなすこともできる． ==参考文献== 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「System F」の詳細全文を読む スポンサード リンク
|